H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.38 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((properFraction :: RealFrac a => a -> (Int,a)) :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((properFraction :: RealFrac a => a -> (Int,a)) :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((properFraction :: RealFrac a => a -> (Int,a)) :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vx vy)

is replaced by the following term

Double vx vy

The bind variable of the following binding Pattern

frac@(Float wv ww)

is replaced by the following term

Float wv ww

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((properFraction :: RealFrac a => a -> (Int,a)) :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((properFraction :: RealFrac a => a -> (Int,a)) :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,wy) = q

r = r0 vu30

r0 (wz,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionQ xv xw = properFractionQ1 xv xw (properFractionVu30 xv xw)

properFractionQ1 xv xw (q,wy) = q

properFractionR xv xw = properFractionR0 xv xw (properFractionVu30 xv xw)

properFractionR0 xv xw (wz,r) = r

properFractionVu30 xv xw = quotRem xv xw

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((properFraction :: RealFrac a => a -> (Int,a)) :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(properFraction :: RealFrac a => a -> (Int,a))

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="properFraction\n  RealFrac a",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="properFraction xx3\n  RealFrac a",fontsize=16,color="blue",shape="box"];690[label="properFraction :: Double -> (@2) Int Double",fontsize=10,color="white",style="solid",shape="box"];3 -> 690[label="",style="solid", color="blue", weight=9];
690 -> 4[label="",style="solid", color="blue", weight=3];
691[label="properFraction :: Float -> (@2) Int Float",fontsize=10,color="white",style="solid",shape="box"];3 -> 691[label="",style="solid", color="blue", weight=9];
691 -> 5[label="",style="solid", color="blue", weight=3];
692[label="properFraction :: (Ratio a) -> (@2) Int (Ratio a)",fontsize=10,color="white",style="solid",shape="box"];3 -> 692[label="",style="solid", color="blue", weight=9];
692 -> 6[label="",style="solid", color="blue", weight=3];
4[label="properFraction xx3",fontsize=16,color="black",shape="box"];4 -> 7[label="",style="solid", color="black", weight=3];
5[label="properFraction xx3",fontsize=16,color="black",shape="box"];5 -> 8[label="",style="solid", color="black", weight=3];
6[label="properFraction xx3\n  Integral a",fontsize=16,color="burlywood",shape="box"];693[label="xx3/xx30 :% xx31",fontsize=10,color="white",style="solid",shape="box"];6 -> 693[label="",style="solid", color="burlywood", weight=9];
693 -> 9[label="",style="solid", color="burlywood", weight=3];
7[label="floatProperFractionDouble xx3",fontsize=16,color="burlywood",shape="box"];694[label="xx3/Double xx30 xx31",fontsize=10,color="white",style="solid",shape="box"];7 -> 694[label="",style="solid", color="burlywood", weight=9];
694 -> 10[label="",style="solid", color="burlywood", weight=3];
8[label="floatProperFractionFloat xx3",fontsize=16,color="burlywood",shape="box"];695[label="xx3/Float xx30 xx31",fontsize=10,color="white",style="solid",shape="box"];8 -> 695[label="",style="solid", color="burlywood", weight=9];
695 -> 11[label="",style="solid", color="burlywood", weight=3];
9[label="properFraction (xx30 :% xx31)\n  Integral a",fontsize=16,color="black",shape="box"];9 -> 12[label="",style="solid", color="black", weight=3];
10[label="floatProperFractionDouble (Double xx30 xx31)",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="floatProperFractionFloat (Float xx30 xx31)",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="(fromIntegral (properFractionQ xx30 xx31),properFractionR xx30 xx31 :% xx31)\n  Integral a",fontsize=16,color="green",shape="box"];12 -> 15[label="",style="dashed", color="green", weight=3];
12 -> 16[label="",style="dashed", color="green", weight=3];
13[label="(fromInt (xx30 `quot` xx31),Double xx30 xx31 - fromInt (xx30 `quot` xx31))",fontsize=16,color="green",shape="box"];13 -> 17[label="",style="dashed", color="green", weight=3];
13 -> 18[label="",style="dashed", color="green", weight=3];
14[label="(fromInt (xx30 `quot` xx31),Float xx30 xx31 - fromInt (xx30 `quot` xx31))",fontsize=16,color="green",shape="box"];14 -> 19[label="",style="dashed", color="green", weight=3];
14 -> 20[label="",style="dashed", color="green", weight=3];
15[label="fromIntegral (properFractionQ xx30 xx31)\n  Integral a",fontsize=16,color="black",shape="box"];15 -> 21[label="",style="solid", color="black", weight=3];
16[label="properFractionR xx30 xx31\n  Integral a",fontsize=16,color="black",shape="box"];16 -> 22[label="",style="solid", color="black", weight=3];
17[label="fromInt (xx30 `quot` xx31)",fontsize=16,color="black",shape="triangle"];17 -> 23[label="",style="solid", color="black", weight=3];
18[label="Double xx30 xx31 - fromInt (xx30 `quot` xx31)",fontsize=16,color="black",shape="box"];18 -> 24[label="",style="solid", color="black", weight=3];
19 -> 17[label="",style="dashed", color="red", weight=0];
19[label="fromInt (xx30 `quot` xx31)",fontsize=16,color="magenta"];19 -> 25[label="",style="dashed", color="magenta", weight=3];
19 -> 26[label="",style="dashed", color="magenta", weight=3];
20[label="Float xx30 xx31 - fromInt (xx30 `quot` xx31)",fontsize=16,color="black",shape="box"];20 -> 27[label="",style="solid", color="black", weight=3];
21[label="fromInteger . toInteger\n  Integral a",fontsize=16,color="black",shape="box"];21 -> 28[label="",style="solid", color="black", weight=3];
22 -> 37[label="",style="dashed", color="red", weight=0];
22[label="properFractionR0 xx30 xx31 (properFractionVu30 xx30 xx31)\n  Integral a",fontsize=16,color="magenta"];22 -> 38[label="",style="dashed", color="magenta", weight=3];
22 -> 39[label="",style="dashed", color="magenta", weight=3];
22 -> 40[label="",style="dashed", color="magenta", weight=3];
23[label="xx30 `quot` xx31",fontsize=16,color="black",shape="triangle"];23 -> 30[label="",style="solid", color="black", weight=3];
24 -> 31[label="",style="dashed", color="red", weight=0];
24[label="primMinusDouble (Double xx30 xx31) (fromInt (xx30 `quot` xx31))",fontsize=16,color="magenta"];24 -> 32[label="",style="dashed", color="magenta", weight=3];
25[label="xx31",fontsize=16,color="green",shape="box"];26[label="xx30",fontsize=16,color="green",shape="box"];27 -> 33[label="",style="dashed", color="red", weight=0];
27[label="primMinusFloat (Float xx30 xx31) (fromInt (xx30 `quot` xx31))",fontsize=16,color="magenta"];27 -> 34[label="",style="dashed", color="magenta", weight=3];
28[label="fromInteger (toInteger (properFractionQ xx30 xx31))\n  Integral a",fontsize=16,color="blue",shape="box"];700[label="toInteger :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];28 -> 700[label="",style="solid", color="blue", weight=9];
700 -> 35[label="",style="solid", color="blue", weight=3];
701[label="toInteger :: Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];28 -> 701[label="",style="solid", color="blue", weight=9];
701 -> 36[label="",style="solid", color="blue", weight=3];
38[label="properFractionVu30 xx30 xx31\n  Integral a",fontsize=16,color="black",shape="triangle"];38 -> 44[label="",style="solid", color="black", weight=3];
39[label="xx31\n  Integral a",fontsize=16,color="green",shape="box"];40[label="xx30\n  Integral a",fontsize=16,color="green",shape="box"];37[label="properFractionR0 xx12 xx13 xx14\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];702[label="xx14/(xx140,xx141)",fontsize=10,color="white",style="solid",shape="box"];37 -> 702[label="",style="solid", color="burlywood", weight=9];
702 -> 45[label="",style="solid", color="burlywood", weight=3];
30[label="primQuotInt xx30 xx31",fontsize=16,color="burlywood",shape="triangle"];703[label="xx30/Pos xx300",fontsize=10,color="white",style="solid",shape="box"];30 -> 703[label="",style="solid", color="burlywood", weight=9];
703 -> 46[label="",style="solid", color="burlywood", weight=3];
704[label="xx30/Neg xx300",fontsize=10,color="white",style="solid",shape="box"];30 -> 704[label="",style="solid", color="burlywood", weight=9];
704 -> 47[label="",style="solid", color="burlywood", weight=3];
32 -> 23[label="",style="dashed", color="red", weight=0];
32[label="xx30 `quot` xx31",fontsize=16,color="magenta"];31[label="primMinusDouble (Double xx30 xx31) (fromInt xx4)",fontsize=16,color="black",shape="triangle"];31 -> 48[label="",style="solid", color="black", weight=3];
34 -> 23[label="",style="dashed", color="red", weight=0];
34[label="xx30 `quot` xx31",fontsize=16,color="magenta"];34 -> 49[label="",style="dashed", color="magenta", weight=3];
34 -> 50[label="",style="dashed", color="magenta", weight=3];
33[label="primMinusFloat (Float xx30 xx31) (fromInt xx5)",fontsize=16,color="black",shape="triangle"];33 -> 51[label="",style="solid", color="black", weight=3];
35[label="fromInteger (toInteger (properFractionQ xx30 xx31))",fontsize=16,color="black",shape="box"];35 -> 52[label="",style="solid", color="black", weight=3];
36[label="fromInteger (toInteger (properFractionQ xx30 xx31))",fontsize=16,color="black",shape="box"];36 -> 53[label="",style="solid", color="black", weight=3];
44[label="quotRem xx30 xx31\n  Integral a",fontsize=16,color="blue",shape="box"];707[label="quotRem :: Int -> Int -> (@2) Int Int",fontsize=10,color="white",style="solid",shape="box"];44 -> 707[label="",style="solid", color="blue", weight=9];
707 -> 54[label="",style="solid", color="blue", weight=3];
708[label="quotRem :: Integer -> Integer -> (@2) Integer Integer",fontsize=10,color="white",style="solid",shape="box"];44 -> 708[label="",style="solid", color="blue", weight=9];
708 -> 55[label="",style="solid", color="blue", weight=3];
45[label="properFractionR0 xx12 xx13 (xx140,xx141)\n  Integral a",fontsize=16,color="black",shape="box"];45 -> 56[label="",style="solid", color="black", weight=3];
46[label="primQuotInt (Pos xx300) xx31",fontsize=16,color="burlywood",shape="box"];709[label="xx31/Pos xx310",fontsize=10,color="white",style="solid",shape="box"];46 -> 709[label="",style="solid", color="burlywood", weight=9];
709 -> 57[label="",style="solid", color="burlywood", weight=3];
710[label="xx31/Neg xx310",fontsize=10,color="white",style="solid",shape="box"];46 -> 710[label="",style="solid", color="burlywood", weight=9];
710 -> 58[label="",style="solid", color="burlywood", weight=3];
47[label="primQuotInt (Neg xx300) xx31",fontsize=16,color="burlywood",shape="box"];711[label="xx31/Pos xx310",fontsize=10,color="white",style="solid",shape="box"];47 -> 711[label="",style="solid", color="burlywood", weight=9];
711 -> 59[label="",style="solid", color="burlywood", weight=3];
712[label="xx31/Neg xx310",fontsize=10,color="white",style="solid",shape="box"];47 -> 712[label="",style="solid", color="burlywood", weight=9];
712 -> 60[label="",style="solid", color="burlywood", weight=3];
48[label="primMinusDouble (Double xx30 xx31) (primIntToDouble xx4)",fontsize=16,color="black",shape="box"];48 -> 61[label="",style="solid", color="black", weight=3];
49[label="xx31",fontsize=16,color="green",shape="box"];50[label="xx30",fontsize=16,color="green",shape="box"];51[label="primMinusFloat (Float xx30 xx31) (primIntToFloat xx5)",fontsize=16,color="black",shape="box"];51 -> 62[label="",style="solid", color="black", weight=3];
52[label="fromInteger (Integer (properFractionQ xx30 xx31))",fontsize=16,color="black",shape="box"];52 -> 63[label="",style="solid", color="black", weight=3];
53[label="fromInteger (properFractionQ xx30 xx31)",fontsize=16,color="black",shape="box"];53 -> 64[label="",style="solid", color="black", weight=3];
54[label="quotRem xx30 xx31",fontsize=16,color="black",shape="box"];54 -> 65[label="",style="solid", color="black", weight=3];
55[label="quotRem xx30 xx31",fontsize=16,color="burlywood",shape="box"];713[label="xx30/Integer xx300",fontsize=10,color="white",style="solid",shape="box"];55 -> 713[label="",style="solid", color="burlywood", weight=9];
713 -> 66[label="",style="solid", color="burlywood", weight=3];
56[label="xx141\n  Integral a",fontsize=16,color="green",shape="box"];57[label="primQuotInt (Pos xx300) (Pos xx310)",fontsize=16,color="burlywood",shape="box"];714[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];57 -> 714[label="",style="solid", color="burlywood", weight=9];
714 -> 67[label="",style="solid", color="burlywood", weight=3];
715[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];57 -> 715[label="",style="solid", color="burlywood", weight=9];
715 -> 68[label="",style="solid", color="burlywood", weight=3];
58[label="primQuotInt (Pos xx300) (Neg xx310)",fontsize=16,color="burlywood",shape="box"];716[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];58 -> 716[label="",style="solid", color="burlywood", weight=9];
716 -> 69[label="",style="solid", color="burlywood", weight=3];
717[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];58 -> 717[label="",style="solid", color="burlywood", weight=9];
717 -> 70[label="",style="solid", color="burlywood", weight=3];
59[label="primQuotInt (Neg xx300) (Pos xx310)",fontsize=16,color="burlywood",shape="box"];718[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];59 -> 718[label="",style="solid", color="burlywood", weight=9];
718 -> 71[label="",style="solid", color="burlywood", weight=3];
719[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];59 -> 719[label="",style="solid", color="burlywood", weight=9];
719 -> 72[label="",style="solid", color="burlywood", weight=3];
60[label="primQuotInt (Neg xx300) (Neg xx310)",fontsize=16,color="burlywood",shape="box"];720[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];60 -> 720[label="",style="solid", color="burlywood", weight=9];
720 -> 73[label="",style="solid", color="burlywood", weight=3];
721[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];60 -> 721[label="",style="solid", color="burlywood", weight=9];
721 -> 74[label="",style="solid", color="burlywood", weight=3];
61[label="primMinusDouble (Double xx30 xx31) (Double xx4 (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];61 -> 75[label="",style="solid", color="black", weight=3];
62[label="primMinusFloat (Float xx30 xx31) (Float xx5 (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];62 -> 76[label="",style="solid", color="black", weight=3];
63[label="properFractionQ xx30 xx31",fontsize=16,color="black",shape="box"];63 -> 77[label="",style="solid", color="black", weight=3];
64 -> 78[label="",style="dashed", color="red", weight=0];
64[label="fromInteger (properFractionQ1 xx30 xx31 (properFractionVu30 xx30 xx31))",fontsize=16,color="magenta"];64 -> 79[label="",style="dashed", color="magenta", weight=3];
65[label="primQrmInt xx30 xx31",fontsize=16,color="black",shape="box"];65 -> 80[label="",style="solid", color="black", weight=3];
66[label="quotRem (Integer xx300) xx31",fontsize=16,color="burlywood",shape="box"];723[label="xx31/Integer xx310",fontsize=10,color="white",style="solid",shape="box"];66 -> 723[label="",style="solid", color="burlywood", weight=9];
723 -> 81[label="",style="solid", color="burlywood", weight=3];
67[label="primQuotInt (Pos xx300) (Pos (Succ xx3100))",fontsize=16,color="black",shape="box"];67 -> 82[label="",style="solid", color="black", weight=3];
68[label="primQuotInt (Pos xx300) (Pos Zero)",fontsize=16,color="black",shape="box"];68 -> 83[label="",style="solid", color="black", weight=3];
69[label="primQuotInt (Pos xx300) (Neg (Succ xx3100))",fontsize=16,color="black",shape="box"];69 -> 84[label="",style="solid", color="black", weight=3];
70[label="primQuotInt (Pos xx300) (Neg Zero)",fontsize=16,color="black",shape="box"];70 -> 85[label="",style="solid", color="black", weight=3];
71[label="primQuotInt (Neg xx300) (Pos (Succ xx3100))",fontsize=16,color="black",shape="box"];71 -> 86[label="",style="solid", color="black", weight=3];
72[label="primQuotInt (Neg xx300) (Pos Zero)",fontsize=16,color="black",shape="box"];72 -> 87[label="",style="solid", color="black", weight=3];
73[label="primQuotInt (Neg xx300) (Neg (Succ xx3100))",fontsize=16,color="black",shape="box"];73 -> 88[label="",style="solid", color="black", weight=3];
74[label="primQuotInt (Neg xx300) (Neg Zero)",fontsize=16,color="black",shape="box"];74 -> 89[label="",style="solid", color="black", weight=3];
75[label="Double (xx30 - xx4) (xx31 * Pos (Succ Zero))",fontsize=16,color="green",shape="box"];75 -> 90[label="",style="dashed", color="green", weight=3];
75 -> 91[label="",style="dashed", color="green", weight=3];
76[label="Float (xx30 - xx5) (xx31 * Pos (Succ Zero))",fontsize=16,color="green",shape="box"];76 -> 92[label="",style="dashed", color="green", weight=3];
76 -> 93[label="",style="dashed", color="green", weight=3];
77 -> 94[label="",style="dashed", color="red", weight=0];
77[label="properFractionQ1 xx30 xx31 (properFractionVu30 xx30 xx31)",fontsize=16,color="magenta"];77 -> 95[label="",style="dashed", color="magenta", weight=3];
79 -> 38[label="",style="dashed", color="red", weight=0];
79[label="properFractionVu30 xx30 xx31",fontsize=16,color="magenta"];78[label="fromInteger (properFractionQ1 xx30 xx31 xx15)",fontsize=16,color="burlywood",shape="triangle"];726[label="xx15/(xx150,xx151)",fontsize=10,color="white",style="solid",shape="box"];78 -> 726[label="",style="solid", color="burlywood", weight=9];
726 -> 96[label="",style="solid", color="burlywood", weight=3];
80[label="(primQuotInt xx30 xx31,primRemInt xx30 xx31)",fontsize=16,color="green",shape="box"];80 -> 97[label="",style="dashed", color="green", weight=3];
80 -> 98[label="",style="dashed", color="green", weight=3];
81[label="quotRem (Integer xx300) (Integer xx310)",fontsize=16,color="black",shape="box"];81 -> 99[label="",style="solid", color="black", weight=3];
82[label="Pos (primDivNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];82 -> 100[label="",style="dashed", color="green", weight=3];
83[label="error []",fontsize=16,color="black",shape="triangle"];83 -> 101[label="",style="solid", color="black", weight=3];
84[label="Neg (primDivNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];84 -> 102[label="",style="dashed", color="green", weight=3];
85 -> 83[label="",style="dashed", color="red", weight=0];
85[label="error []",fontsize=16,color="magenta"];86[label="Neg (primDivNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];86 -> 103[label="",style="dashed", color="green", weight=3];
87 -> 83[label="",style="dashed", color="red", weight=0];
87[label="error []",fontsize=16,color="magenta"];88[label="Pos (primDivNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];88 -> 104[label="",style="dashed", color="green", weight=3];
89 -> 83[label="",style="dashed", color="red", weight=0];
89[label="error []",fontsize=16,color="magenta"];90[label="xx30 - xx4",fontsize=16,color="black",shape="triangle"];90 -> 105[label="",style="solid", color="black", weight=3];
91[label="xx31 * Pos (Succ Zero)",fontsize=16,color="black",shape="triangle"];91 -> 106[label="",style="solid", color="black", weight=3];
92 -> 90[label="",style="dashed", color="red", weight=0];
92[label="xx30 - xx5",fontsize=16,color="magenta"];92 -> 107[label="",style="dashed", color="magenta", weight=3];
92 -> 108[label="",style="dashed", color="magenta", weight=3];
93 -> 91[label="",style="dashed", color="red", weight=0];
93[label="xx31 * Pos (Succ Zero)",fontsize=16,color="magenta"];93 -> 109[label="",style="dashed", color="magenta", weight=3];
95 -> 38[label="",style="dashed", color="red", weight=0];
95[label="properFractionVu30 xx30 xx31",fontsize=16,color="magenta"];94[label="properFractionQ1 xx30 xx31 xx16",fontsize=16,color="burlywood",shape="triangle"];733[label="xx16/(xx160,xx161)",fontsize=10,color="white",style="solid",shape="box"];94 -> 733[label="",style="solid", color="burlywood", weight=9];
733 -> 110[label="",style="solid", color="burlywood", weight=3];
96[label="fromInteger (properFractionQ1 xx30 xx31 (xx150,xx151))",fontsize=16,color="black",shape="box"];96 -> 111[label="",style="solid", color="black", weight=3];
97 -> 30[label="",style="dashed", color="red", weight=0];
97[label="primQuotInt xx30 xx31",fontsize=16,color="magenta"];97 -> 112[label="",style="dashed", color="magenta", weight=3];
97 -> 113[label="",style="dashed", color="magenta", weight=3];
98[label="primRemInt xx30 xx31",fontsize=16,color="burlywood",shape="triangle"];735[label="xx30/Pos xx300",fontsize=10,color="white",style="solid",shape="box"];98 -> 735[label="",style="solid", color="burlywood", weight=9];
735 -> 114[label="",style="solid", color="burlywood", weight=3];
736[label="xx30/Neg xx300",fontsize=10,color="white",style="solid",shape="box"];98 -> 736[label="",style="solid", color="burlywood", weight=9];
736 -> 115[label="",style="solid", color="burlywood", weight=3];
99[label="(Integer (primQuotInt xx300 xx310),Integer (primRemInt xx300 xx310))",fontsize=16,color="green",shape="box"];99 -> 116[label="",style="dashed", color="green", weight=3];
99 -> 117[label="",style="dashed", color="green", weight=3];
100[label="primDivNatS xx300 (Succ xx3100)",fontsize=16,color="burlywood",shape="triangle"];737[label="xx300/Succ xx3000",fontsize=10,color="white",style="solid",shape="box"];100 -> 737[label="",style="solid", color="burlywood", weight=9];
737 -> 118[label="",style="solid", color="burlywood", weight=3];
738[label="xx300/Zero",fontsize=10,color="white",style="solid",shape="box"];100 -> 738[label="",style="solid", color="burlywood", weight=9];
738 -> 119[label="",style="solid", color="burlywood", weight=3];
101[label="error []",fontsize=16,color="red",shape="box"];102 -> 100[label="",style="dashed", color="red", weight=0];
102[label="primDivNatS xx300 (Succ xx3100)",fontsize=16,color="magenta"];102 -> 120[label="",style="dashed", color="magenta", weight=3];
103 -> 100[label="",style="dashed", color="red", weight=0];
103[label="primDivNatS xx300 (Succ xx3100)",fontsize=16,color="magenta"];103 -> 121[label="",style="dashed", color="magenta", weight=3];
104 -> 100[label="",style="dashed", color="red", weight=0];
104[label="primDivNatS xx300 (Succ xx3100)",fontsize=16,color="magenta"];104 -> 122[label="",style="dashed", color="magenta", weight=3];
104 -> 123[label="",style="dashed", color="magenta", weight=3];
105[label="primMinusInt xx30 xx4",fontsize=16,color="burlywood",shape="box"];742[label="xx30/Pos xx300",fontsize=10,color="white",style="solid",shape="box"];105 -> 742[label="",style="solid", color="burlywood", weight=9];
742 -> 124[label="",style="solid", color="burlywood", weight=3];
743[label="xx30/Neg xx300",fontsize=10,color="white",style="solid",shape="box"];105 -> 743[label="",style="solid", color="burlywood", weight=9];
743 -> 125[label="",style="solid", color="burlywood", weight=3];
106[label="primMulInt xx31 (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];744[label="xx31/Pos xx310",fontsize=10,color="white",style="solid",shape="box"];106 -> 744[label="",style="solid", color="burlywood", weight=9];
744 -> 126[label="",style="solid", color="burlywood", weight=3];
745[label="xx31/Neg xx310",fontsize=10,color="white",style="solid",shape="box"];106 -> 745[label="",style="solid", color="burlywood", weight=9];
745 -> 127[label="",style="solid", color="burlywood", weight=3];
107[label="xx30",fontsize=16,color="green",shape="box"];108[label="xx5",fontsize=16,color="green",shape="box"];109[label="xx31",fontsize=16,color="green",shape="box"];110[label="properFractionQ1 xx30 xx31 (xx160,xx161)",fontsize=16,color="black",shape="box"];110 -> 128[label="",style="solid", color="black", weight=3];
111[label="fromInteger xx150",fontsize=16,color="burlywood",shape="box"];746[label="xx150/Integer xx1500",fontsize=10,color="white",style="solid",shape="box"];111 -> 746[label="",style="solid", color="burlywood", weight=9];
746 -> 129[label="",style="solid", color="burlywood", weight=3];
112[label="xx31",fontsize=16,color="green",shape="box"];113[label="xx30",fontsize=16,color="green",shape="box"];114[label="primRemInt (Pos xx300) xx31",fontsize=16,color="burlywood",shape="box"];747[label="xx31/Pos xx310",fontsize=10,color="white",style="solid",shape="box"];114 -> 747[label="",style="solid", color="burlywood", weight=9];
747 -> 130[label="",style="solid", color="burlywood", weight=3];
748[label="xx31/Neg xx310",fontsize=10,color="white",style="solid",shape="box"];114 -> 748[label="",style="solid", color="burlywood", weight=9];
748 -> 131[label="",style="solid", color="burlywood", weight=3];
115[label="primRemInt (Neg xx300) xx31",fontsize=16,color="burlywood",shape="box"];749[label="xx31/Pos xx310",fontsize=10,color="white",style="solid",shape="box"];115 -> 749[label="",style="solid", color="burlywood", weight=9];
749 -> 132[label="",style="solid", color="burlywood", weight=3];
750[label="xx31/Neg xx310",fontsize=10,color="white",style="solid",shape="box"];115 -> 750[label="",style="solid", color="burlywood", weight=9];
750 -> 133[label="",style="solid", color="burlywood", weight=3];
116 -> 30[label="",style="dashed", color="red", weight=0];
116[label="primQuotInt xx300 xx310",fontsize=16,color="magenta"];116 -> 134[label="",style="dashed", color="magenta", weight=3];
116 -> 135[label="",style="dashed", color="magenta", weight=3];
117 -> 98[label="",style="dashed", color="red", weight=0];
117[label="primRemInt xx300 xx310",fontsize=16,color="magenta"];117 -> 136[label="",style="dashed", color="magenta", weight=3];
117 -> 137[label="",style="dashed", color="magenta", weight=3];
118[label="primDivNatS (Succ xx3000) (Succ xx3100)",fontsize=16,color="black",shape="box"];118 -> 138[label="",style="solid", color="black", weight=3];
119[label="primDivNatS Zero (Succ xx3100)",fontsize=16,color="black",shape="box"];119 -> 139[label="",style="solid", color="black", weight=3];
120[label="xx3100",fontsize=16,color="green",shape="box"];121[label="xx300",fontsize=16,color="green",shape="box"];122[label="xx300",fontsize=16,color="green",shape="box"];123[label="xx3100",fontsize=16,color="green",shape="box"];124[label="primMinusInt (Pos xx300) xx4",fontsize=16,color="burlywood",shape="box"];753[label="xx4/Pos xx40",fontsize=10,color="white",style="solid",shape="box"];124 -> 753[label="",style="solid", color="burlywood", weight=9];
753 -> 140[label="",style="solid", color="burlywood", weight=3];
754[label="xx4/Neg xx40",fontsize=10,color="white",style="solid",shape="box"];124 -> 754[label="",style="solid", color="burlywood", weight=9];
754 -> 141[label="",style="solid", color="burlywood", weight=3];
125[label="primMinusInt (Neg xx300) xx4",fontsize=16,color="burlywood",shape="box"];755[label="xx4/Pos xx40",fontsize=10,color="white",style="solid",shape="box"];125 -> 755[label="",style="solid", color="burlywood", weight=9];
755 -> 142[label="",style="solid", color="burlywood", weight=3];
756[label="xx4/Neg xx40",fontsize=10,color="white",style="solid",shape="box"];125 -> 756[label="",style="solid", color="burlywood", weight=9];
756 -> 143[label="",style="solid", color="burlywood", weight=3];
126[label="primMulInt (Pos xx310) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];126 -> 144[label="",style="solid", color="black", weight=3];
127[label="primMulInt (Neg xx310) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];127 -> 145[label="",style="solid", color="black", weight=3];
128[label="xx160",fontsize=16,color="green",shape="box"];129[label="fromInteger (Integer xx1500)",fontsize=16,color="black",shape="box"];129 -> 146[label="",style="solid", color="black", weight=3];
130[label="primRemInt (Pos xx300) (Pos xx310)",fontsize=16,color="burlywood",shape="box"];757[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];130 -> 757[label="",style="solid", color="burlywood", weight=9];
757 -> 147[label="",style="solid", color="burlywood", weight=3];
758[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];130 -> 758[label="",style="solid", color="burlywood", weight=9];
758 -> 148[label="",style="solid", color="burlywood", weight=3];
131[label="primRemInt (Pos xx300) (Neg xx310)",fontsize=16,color="burlywood",shape="box"];759[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];131 -> 759[label="",style="solid", color="burlywood", weight=9];
759 -> 149[label="",style="solid", color="burlywood", weight=3];
760[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];131 -> 760[label="",style="solid", color="burlywood", weight=9];
760 -> 150[label="",style="solid", color="burlywood", weight=3];
132[label="primRemInt (Neg xx300) (Pos xx310)",fontsize=16,color="burlywood",shape="box"];761[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];132 -> 761[label="",style="solid", color="burlywood", weight=9];
761 -> 151[label="",style="solid", color="burlywood", weight=3];
762[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];132 -> 762[label="",style="solid", color="burlywood", weight=9];
762 -> 152[label="",style="solid", color="burlywood", weight=3];
133[label="primRemInt (Neg xx300) (Neg xx310)",fontsize=16,color="burlywood",shape="box"];763[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];133 -> 763[label="",style="solid", color="burlywood", weight=9];
763 -> 153[label="",style="solid", color="burlywood", weight=3];
764[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];133 -> 764[label="",style="solid", color="burlywood", weight=9];
764 -> 154[label="",style="solid", color="burlywood", weight=3];
134[label="xx310",fontsize=16,color="green",shape="box"];135[label="xx300",fontsize=16,color="green",shape="box"];136[label="xx310",fontsize=16,color="green",shape="box"];137[label="xx300",fontsize=16,color="green",shape="box"];138[label="primDivNatS0 xx3000 xx3100 (primGEqNatS xx3000 xx3100)",fontsize=16,color="burlywood",shape="box"];765[label="xx3000/Succ xx30000",fontsize=10,color="white",style="solid",shape="box"];138 -> 765[label="",style="solid", color="burlywood", weight=9];
765 -> 155[label="",style="solid", color="burlywood", weight=3];
766[label="xx3000/Zero",fontsize=10,color="white",style="solid",shape="box"];138 -> 766[label="",style="solid", color="burlywood", weight=9];
766 -> 156[label="",style="solid", color="burlywood", weight=3];
139[label="Zero",fontsize=16,color="green",shape="box"];140[label="primMinusInt (Pos xx300) (Pos xx40)",fontsize=16,color="black",shape="box"];140 -> 157[label="",style="solid", color="black", weight=3];
141[label="primMinusInt (Pos xx300) (Neg xx40)",fontsize=16,color="black",shape="box"];141 -> 158[label="",style="solid", color="black", weight=3];
142[label="primMinusInt (Neg xx300) (Pos xx40)",fontsize=16,color="black",shape="box"];142 -> 159[label="",style="solid", color="black", weight=3];
143[label="primMinusInt (Neg xx300) (Neg xx40)",fontsize=16,color="black",shape="box"];143 -> 160[label="",style="solid", color="black", weight=3];
144[label="Pos (primMulNat xx310 (Succ Zero))",fontsize=16,color="green",shape="box"];144 -> 161[label="",style="dashed", color="green", weight=3];
145[label="Neg (primMulNat xx310 (Succ Zero))",fontsize=16,color="green",shape="box"];145 -> 162[label="",style="dashed", color="green", weight=3];
146[label="xx1500",fontsize=16,color="green",shape="box"];147[label="primRemInt (Pos xx300) (Pos (Succ xx3100))",fontsize=16,color="black",shape="box"];147 -> 163[label="",style="solid", color="black", weight=3];
148[label="primRemInt (Pos xx300) (Pos Zero)",fontsize=16,color="black",shape="box"];148 -> 164[label="",style="solid", color="black", weight=3];
149[label="primRemInt (Pos xx300) (Neg (Succ xx3100))",fontsize=16,color="black",shape="box"];149 -> 165[label="",style="solid", color="black", weight=3];
150[label="primRemInt (Pos xx300) (Neg Zero)",fontsize=16,color="black",shape="box"];150 -> 166[label="",style="solid", color="black", weight=3];
151[label="primRemInt (Neg xx300) (Pos (Succ xx3100))",fontsize=16,color="black",shape="box"];151 -> 167[label="",style="solid", color="black", weight=3];
152[label="primRemInt (Neg xx300) (Pos Zero)",fontsize=16,color="black",shape="box"];152 -> 168[label="",style="solid", color="black", weight=3];
153[label="primRemInt (Neg xx300) (Neg (Succ xx3100))",fontsize=16,color="black",shape="box"];153 -> 169[label="",style="solid", color="black", weight=3];
154[label="primRemInt (Neg xx300) (Neg Zero)",fontsize=16,color="black",shape="box"];154 -> 170[label="",style="solid", color="black", weight=3];
155[label="primDivNatS0 (Succ xx30000) xx3100 (primGEqNatS (Succ xx30000) xx3100)",fontsize=16,color="burlywood",shape="box"];767[label="xx3100/Succ xx31000",fontsize=10,color="white",style="solid",shape="box"];155 -> 767[label="",style="solid", color="burlywood", weight=9];
767 -> 171[label="",style="solid", color="burlywood", weight=3];
768[label="xx3100/Zero",fontsize=10,color="white",style="solid",shape="box"];155 -> 768[label="",style="solid", color="burlywood", weight=9];
768 -> 172[label="",style="solid", color="burlywood", weight=3];
156[label="primDivNatS0 Zero xx3100 (primGEqNatS Zero xx3100)",fontsize=16,color="burlywood",shape="box"];769[label="xx3100/Succ xx31000",fontsize=10,color="white",style="solid",shape="box"];156 -> 769[label="",style="solid", color="burlywood", weight=9];
769 -> 173[label="",style="solid", color="burlywood", weight=3];
770[label="xx3100/Zero",fontsize=10,color="white",style="solid",shape="box"];156 -> 770[label="",style="solid", color="burlywood", weight=9];
770 -> 174[label="",style="solid", color="burlywood", weight=3];
157[label="primMinusNat xx300 xx40",fontsize=16,color="burlywood",shape="triangle"];771[label="xx300/Succ xx3000",fontsize=10,color="white",style="solid",shape="box"];157 -> 771[label="",style="solid", color="burlywood", weight=9];
771 -> 175[label="",style="solid", color="burlywood", weight=3];
772[label="xx300/Zero",fontsize=10,color="white",style="solid",shape="box"];157 -> 772[label="",style="solid", color="burlywood", weight=9];
772 -> 176[label="",style="solid", color="burlywood", weight=3];
158[label="Pos (primPlusNat xx300 xx40)",fontsize=16,color="green",shape="box"];158 -> 177[label="",style="dashed", color="green", weight=3];
159[label="Neg (primPlusNat xx300 xx40)",fontsize=16,color="green",shape="box"];159 -> 178[label="",style="dashed", color="green", weight=3];
160 -> 157[label="",style="dashed", color="red", weight=0];
160[label="primMinusNat xx40 xx300",fontsize=16,color="magenta"];160 -> 179[label="",style="dashed", color="magenta", weight=3];
160 -> 180[label="",style="dashed", color="magenta", weight=3];
161[label="primMulNat xx310 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];774[label="xx310/Succ xx3100",fontsize=10,color="white",style="solid",shape="box"];161 -> 774[label="",style="solid", color="burlywood", weight=9];
774 -> 181[label="",style="solid", color="burlywood", weight=3];
775[label="xx310/Zero",fontsize=10,color="white",style="solid",shape="box"];161 -> 775[label="",style="solid", color="burlywood", weight=9];
775 -> 182[label="",style="solid", color="burlywood", weight=3];
162 -> 161[label="",style="dashed", color="red", weight=0];
162[label="primMulNat xx310 (Succ Zero)",fontsize=16,color="magenta"];162 -> 183[label="",style="dashed", color="magenta", weight=3];
163[label="Pos (primModNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];163 -> 184[label="",style="dashed", color="green", weight=3];
164 -> 83[label="",style="dashed", color="red", weight=0];
164[label="error []",fontsize=16,color="magenta"];165[label="Pos (primModNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];165 -> 185[label="",style="dashed", color="green", weight=3];
166 -> 83[label="",style="dashed", color="red", weight=0];
166[label="error []",fontsize=16,color="magenta"];167[label="Neg (primModNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];167 -> 186[label="",style="dashed", color="green", weight=3];
168 -> 83[label="",style="dashed", color="red", weight=0];
168[label="error []",fontsize=16,color="magenta"];169[label="Neg (primModNatS xx300 (Succ xx3100))",fontsize=16,color="green",shape="box"];169 -> 187[label="",style="dashed", color="green", weight=3];
170 -> 83[label="",style="dashed", color="red", weight=0];
170[label="error []",fontsize=16,color="magenta"];171[label="primDivNatS0 (Succ xx30000) (Succ xx31000) (primGEqNatS (Succ xx30000) (Succ xx31000))",fontsize=16,color="black",shape="box"];171 -> 188[label="",style="solid", color="black", weight=3];
172[label="primDivNatS0 (Succ xx30000) Zero (primGEqNatS (Succ xx30000) Zero)",fontsize=16,color="black",shape="box"];172 -> 189[label="",style="solid", color="black", weight=3];
173[label="primDivNatS0 Zero (Succ xx31000) (primGEqNatS Zero (Succ xx31000))",fontsize=16,color="black",shape="box"];173 -> 190[label="",style="solid", color="black", weight=3];
174[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];174 -> 191[label="",style="solid", color="black", weight=3];
175[label="primMinusNat (Succ xx3000) xx40",fontsize=16,color="burlywood",shape="box"];781[label="xx40/Succ xx400",fontsize=10,color="white",style="solid",shape="box"];175 -> 781[label="",style="solid", color="burlywood", weight=9];
781 -> 192[label="",style="solid", color="burlywood", weight=3];
782[label="xx40/Zero",fontsize=10,color="white",style="solid",shape="box"];175 -> 782[label="",style="solid", color="burlywood", weight=9];
782 -> 193[label="",style="solid", color="burlywood", weight=3];
176[label="primMinusNat Zero xx40",fontsize=16,color="burlywood",shape="box"];783[label="xx40/Succ xx400",fontsize=10,color="white",style="solid",shape="box"];176 -> 783[label="",style="solid", color="burlywood", weight=9];
783 -> 194[label="",style="solid", color="burlywood", weight=3];
784[label="xx40/Zero",fontsize=10,color="white",style="solid",shape="box"];176 -> 784[label="",style="solid", color="burlywood", weight=9];
784 -> 195[label="",style="solid", color="burlywood", weight=3];
177[label="primPlusNat xx300 xx40",fontsize=16,color="burlywood",shape="triangle"];785[label="xx300/Succ xx3000",fontsize=10,color="white",style="solid",shape="box"];177 -> 785[label="",style="solid", color="burlywood", weight=9];
785 -> 196[label="",style="solid", color="burlywood", weight=3];
786[label="xx300/Zero",fontsize=10,color="white",style="solid",shape="box"];177 -> 786[label="",style="solid", color="burlywood", weight=9];
786 -> 197[label="",style="solid", color="burlywood", weight=3];
178 -> 177[label="",style="dashed", color="red", weight=0];
178[label="primPlusNat xx300 xx40",fontsize=16,color="magenta"];178 -> 198[label="",style="dashed", color="magenta", weight=3];
178 -> 199[label="",style="dashed", color="magenta", weight=3];
179[label="xx40",fontsize=16,color="green",shape="box"];180[label="xx300",fontsize=16,color="green",shape="box"];181[label="primMulNat (Succ xx3100) (Succ Zero)",fontsize=16,color="black",shape="box"];181 -> 200[label="",style="solid", color="black", weight=3];
182[label="primMulNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];182 -> 201[label="",style="solid", color="black", weight=3];
183[label="xx310",fontsize=16,color="green",shape="box"];184[label="primModNatS xx300 (Succ xx3100)",fontsize=16,color="burlywood",shape="triangle"];788[label="xx300/Succ xx3000",fontsize=10,color="white",style="solid",shape="box"];184 -> 788[label="",style="solid", color="burlywood", weight=9];
788 -> 202[label="",style="solid", color="burlywood", weight=3];
789[label="xx300/Zero",fontsize=10,color="white",style="solid",shape="box"];184 -> 789[label="",style="solid", color="burlywood", weight=9];
789 -> 203[label="",style="solid", color="burlywood", weight=3];
185 -> 184[label="",style="dashed", color="red", weight=0];
185[label="primModNatS xx300 (Succ xx3100)",fontsize=16,color="magenta"];185 -> 204[label="",style="dashed", color="magenta", weight=3];
186 -> 184[label="",style="dashed", color="red", weight=0];
186[label="primModNatS xx300 (Succ xx3100)",fontsize=16,color="magenta"];186 -> 205[label="",style="dashed", color="magenta", weight=3];
187 -> 184[label="",style="dashed", color="red", weight=0];
187[label="primModNatS xx300 (Succ xx3100)",fontsize=16,color="magenta"];187 -> 206[label="",style="dashed", color="magenta", weight=3];
187 -> 207[label="",style="dashed", color="magenta", weight=3];
188 -> 491[label="",style="dashed", color="red", weight=0];
188[label="primDivNatS0 (Succ xx30000) (Succ xx31000) (primGEqNatS xx30000 xx31000)",fontsize=16,color="magenta"];188 -> 492[label="",style="dashed", color="magenta", weight=3];
188 -> 493[label="",style="dashed", color="magenta", weight=3];
188 -> 494[label="",style="dashed", color="magenta", weight=3];
188 -> 495[label="",style="dashed", color="magenta", weight=3];
189[label="primDivNatS0 (Succ xx30000) Zero True",fontsize=16,color="black",shape="box"];189 -> 210[label="",style="solid", color="black", weight=3];
190[label="primDivNatS0 Zero (Succ xx31000) False",fontsize=16,color="black",shape="box"];190 -> 211[label="",style="solid", color="black", weight=3];
191[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];191 -> 212[label="",style="solid", color="black", weight=3];
192[label="primMinusNat (Succ xx3000) (Succ xx400)",fontsize=16,color="black",shape="box"];192 -> 213[label="",style="solid", color="black", weight=3];
193[label="primMinusNat (Succ xx3000) Zero",fontsize=16,color="black",shape="box"];193 -> 214[label="",style="solid", color="black", weight=3];
194[label="primMinusNat Zero (Succ xx400)",fontsize=16,color="black",shape="box"];194 -> 215[label="",style="solid", color="black", weight=3];
195[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];195 -> 216[label="",style="solid", color="black", weight=3];
196[label="primPlusNat (Succ xx3000) xx40",fontsize=16,color="burlywood",shape="box"];794[label="xx40/Succ xx400",fontsize=10,color="white",style="solid",shape="box"];196 -> 794[label="",style="solid", color="burlywood", weight=9];
794 -> 217[label="",style="solid", color="burlywood", weight=3];
795[label="xx40/Zero",fontsize=10,color="white",style="solid",shape="box"];196 -> 795[label="",style="solid", color="burlywood", weight=9];
795 -> 218[label="",style="solid", color="burlywood", weight=3];
197[label="primPlusNat Zero xx40",fontsize=16,color="burlywood",shape="box"];796[label="xx40/Succ xx400",fontsize=10,color="white",style="solid",shape="box"];197 -> 796[label="",style="solid", color="burlywood", weight=9];
796 -> 219[label="",style="solid", color="burlywood", weight=3];
797[label="xx40/Zero",fontsize=10,color="white",style="solid",shape="box"];197 -> 797[label="",style="solid", color="burlywood", weight=9];
797 -> 220[label="",style="solid", color="burlywood", weight=3];
198[label="xx300",fontsize=16,color="green",shape="box"];199[label="xx40",fontsize=16,color="green",shape="box"];200 -> 177[label="",style="dashed", color="red", weight=0];
200[label="primPlusNat (primMulNat xx3100 (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];200 -> 221[label="",style="dashed", color="magenta", weight=3];
200 -> 222[label="",style="dashed", color="magenta", weight=3];
201[label="Zero",fontsize=16,color="green",shape="box"];202[label="primModNatS (Succ xx3000) (Succ xx3100)",fontsize=16,color="black",shape="box"];202 -> 223[label="",style="solid", color="black", weight=3];
203[label="primModNatS Zero (Succ xx3100)",fontsize=16,color="black",shape="box"];203 -> 224[label="",style="solid", color="black", weight=3];
204[label="xx3100",fontsize=16,color="green",shape="box"];205[label="xx300",fontsize=16,color="green",shape="box"];206[label="xx3100",fontsize=16,color="green",shape="box"];207[label="xx300",fontsize=16,color="green",shape="box"];492[label="xx30000",fontsize=16,color="green",shape="box"];493[label="xx31000",fontsize=16,color="green",shape="box"];494[label="xx31000",fontsize=16,color="green",shape="box"];495[label="xx30000",fontsize=16,color="green",shape="box"];491[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS xx35 xx36)",fontsize=16,color="burlywood",shape="triangle"];799[label="xx35/Succ xx350",fontsize=10,color="white",style="solid",shape="box"];491 -> 799[label="",style="solid", color="burlywood", weight=9];
799 -> 524[label="",style="solid", color="burlywood", weight=3];
800[label="xx35/Zero",fontsize=10,color="white",style="solid",shape="box"];491 -> 800[label="",style="solid", color="burlywood", weight=9];
800 -> 525[label="",style="solid", color="burlywood", weight=3];
210[label="Succ (primDivNatS (primMinusNatS (Succ xx30000) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];210 -> 229[label="",style="dashed", color="green", weight=3];
211[label="Zero",fontsize=16,color="green",shape="box"];212[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];212 -> 230[label="",style="dashed", color="green", weight=3];
213 -> 157[label="",style="dashed", color="red", weight=0];
213[label="primMinusNat xx3000 xx400",fontsize=16,color="magenta"];213 -> 231[label="",style="dashed", color="magenta", weight=3];
213 -> 232[label="",style="dashed", color="magenta", weight=3];
214[label="Pos (Succ xx3000)",fontsize=16,color="green",shape="box"];215[label="Neg (Succ xx400)",fontsize=16,color="green",shape="box"];216[label="Pos Zero",fontsize=16,color="green",shape="box"];217[label="primPlusNat (Succ xx3000) (Succ xx400)",fontsize=16,color="black",shape="box"];217 -> 233[label="",style="solid", color="black", weight=3];
218[label="primPlusNat (Succ xx3000) Zero",fontsize=16,color="black",shape="box"];218 -> 234[label="",style="solid", color="black", weight=3];
219[label="primPlusNat Zero (Succ xx400)",fontsize=16,color="black",shape="box"];219 -> 235[label="",style="solid", color="black", weight=3];
220[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];220 -> 236[label="",style="solid", color="black", weight=3];
221 -> 161[label="",style="dashed", color="red", weight=0];
221[label="primMulNat xx3100 (Succ Zero)",fontsize=16,color="magenta"];221 -> 237[label="",style="dashed", color="magenta", weight=3];
222[label="Succ Zero",fontsize=16,color="green",shape="box"];223[label="primModNatS0 xx3000 xx3100 (primGEqNatS xx3000 xx3100)",fontsize=16,color="burlywood",shape="box"];803[label="xx3000/Succ xx30000",fontsize=10,color="white",style="solid",shape="box"];223 -> 803[label="",style="solid", color="burlywood", weight=9];
803 -> 238[label="",style="solid", color="burlywood", weight=3];
804[label="xx3000/Zero",fontsize=10,color="white",style="solid",shape="box"];223 -> 804[label="",style="solid", color="burlywood", weight=9];
804 -> 239[label="",style="solid", color="burlywood", weight=3];
224[label="Zero",fontsize=16,color="green",shape="box"];524[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS (Succ xx350) xx36)",fontsize=16,color="burlywood",shape="box"];805[label="xx36/Succ xx360",fontsize=10,color="white",style="solid",shape="box"];524 -> 805[label="",style="solid", color="burlywood", weight=9];
805 -> 531[label="",style="solid", color="burlywood", weight=3];
806[label="xx36/Zero",fontsize=10,color="white",style="solid",shape="box"];524 -> 806[label="",style="solid", color="burlywood", weight=9];
806 -> 532[label="",style="solid", color="burlywood", weight=3];
525[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS Zero xx36)",fontsize=16,color="burlywood",shape="box"];807[label="xx36/Succ xx360",fontsize=10,color="white",style="solid",shape="box"];525 -> 807[label="",style="solid", color="burlywood", weight=9];
807 -> 533[label="",style="solid", color="burlywood", weight=3];
808[label="xx36/Zero",fontsize=10,color="white",style="solid",shape="box"];525 -> 808[label="",style="solid", color="burlywood", weight=9];
808 -> 534[label="",style="solid", color="burlywood", weight=3];
229 -> 100[label="",style="dashed", color="red", weight=0];
229[label="primDivNatS (primMinusNatS (Succ xx30000) Zero) (Succ Zero)",fontsize=16,color="magenta"];229 -> 244[label="",style="dashed", color="magenta", weight=3];
229 -> 245[label="",style="dashed", color="magenta", weight=3];
230 -> 100[label="",style="dashed", color="red", weight=0];
230[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];230 -> 246[label="",style="dashed", color="magenta", weight=3];
230 -> 247[label="",style="dashed", color="magenta", weight=3];
231[label="xx3000",fontsize=16,color="green",shape="box"];232[label="xx400",fontsize=16,color="green",shape="box"];233[label="Succ (Succ (primPlusNat xx3000 xx400))",fontsize=16,color="green",shape="box"];233 -> 248[label="",style="dashed", color="green", weight=3];
234[label="Succ xx3000",fontsize=16,color="green",shape="box"];235[label="Succ xx400",fontsize=16,color="green",shape="box"];236[label="Zero",fontsize=16,color="green",shape="box"];237[label="xx3100",fontsize=16,color="green",shape="box"];238[label="primModNatS0 (Succ xx30000) xx3100 (primGEqNatS (Succ xx30000) xx3100)",fontsize=16,color="burlywood",shape="box"];811[label="xx3100/Succ xx31000",fontsize=10,color="white",style="solid",shape="box"];238 -> 811[label="",style="solid", color="burlywood", weight=9];
811 -> 249[label="",style="solid", color="burlywood", weight=3];
812[label="xx3100/Zero",fontsize=10,color="white",style="solid",shape="box"];238 -> 812[label="",style="solid", color="burlywood", weight=9];
812 -> 250[label="",style="solid", color="burlywood", weight=3];
239[label="primModNatS0 Zero xx3100 (primGEqNatS Zero xx3100)",fontsize=16,color="burlywood",shape="box"];813[label="xx3100/Succ xx31000",fontsize=10,color="white",style="solid",shape="box"];239 -> 813[label="",style="solid", color="burlywood", weight=9];
813 -> 251[label="",style="solid", color="burlywood", weight=3];
814[label="xx3100/Zero",fontsize=10,color="white",style="solid",shape="box"];239 -> 814[label="",style="solid", color="burlywood", weight=9];
814 -> 252[label="",style="solid", color="burlywood", weight=3];
531[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS (Succ xx350) (Succ xx360))",fontsize=16,color="black",shape="box"];531 -> 537[label="",style="solid", color="black", weight=3];
532[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS (Succ xx350) Zero)",fontsize=16,color="black",shape="box"];532 -> 538[label="",style="solid", color="black", weight=3];
533[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS Zero (Succ xx360))",fontsize=16,color="black",shape="box"];533 -> 539[label="",style="solid", color="black", weight=3];
534[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];534 -> 540[label="",style="solid", color="black", weight=3];
244[label="primMinusNatS (Succ xx30000) Zero",fontsize=16,color="black",shape="triangle"];244 -> 258[label="",style="solid", color="black", weight=3];
245[label="Zero",fontsize=16,color="green",shape="box"];246[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="triangle"];246 -> 259[label="",style="solid", color="black", weight=3];
247[label="Zero",fontsize=16,color="green",shape="box"];248 -> 177[label="",style="dashed", color="red", weight=0];
248[label="primPlusNat xx3000 xx400",fontsize=16,color="magenta"];248 -> 260[label="",style="dashed", color="magenta", weight=3];
248 -> 261[label="",style="dashed", color="magenta", weight=3];
249[label="primModNatS0 (Succ xx30000) (Succ xx31000) (primGEqNatS (Succ xx30000) (Succ xx31000))",fontsize=16,color="black",shape="box"];249 -> 262[label="",style="solid", color="black", weight=3];
250[label="primModNatS0 (Succ xx30000) Zero (primGEqNatS (Succ xx30000) Zero)",fontsize=16,color="black",shape="box"];250 -> 263[label="",style="solid", color="black", weight=3];
251[label="primModNatS0 Zero (Succ xx31000) (primGEqNatS Zero (Succ xx31000))",fontsize=16,color="black",shape="box"];251 -> 264[label="",style="solid", color="black", weight=3];
252[label="primModNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];252 -> 265[label="",style="solid", color="black", weight=3];
537 -> 491[label="",style="dashed", color="red", weight=0];
537[label="primDivNatS0 (Succ xx33) (Succ xx34) (primGEqNatS xx350 xx360)",fontsize=16,color="magenta"];537 -> 548[label="",style="dashed", color="magenta", weight=3];
537 -> 549[label="",style="dashed", color="magenta", weight=3];
538[label="primDivNatS0 (Succ xx33) (Succ xx34) True",fontsize=16,color="black",shape="triangle"];538 -> 550[label="",style="solid", color="black", weight=3];
539[label="primDivNatS0 (Succ xx33) (Succ xx34) False",fontsize=16,color="black",shape="box"];539 -> 551[label="",style="solid", color="black", weight=3];
540 -> 538[label="",style="dashed", color="red", weight=0];
540[label="primDivNatS0 (Succ xx33) (Succ xx34) True",fontsize=16,color="magenta"];258[label="Succ xx30000",fontsize=16,color="green",shape="box"];259[label="Zero",fontsize=16,color="green",shape="box"];260[label="xx3000",fontsize=16,color="green",shape="box"];261[label="xx400",fontsize=16,color="green",shape="box"];262 -> 635[label="",style="dashed", color="red", weight=0];
262[label="primModNatS0 (Succ xx30000) (Succ xx31000) (primGEqNatS xx30000 xx31000)",fontsize=16,color="magenta"];262 -> 636[label="",style="dashed", color="magenta", weight=3];
262 -> 637[label="",style="dashed", color="magenta", weight=3];
262 -> 638[label="",style="dashed", color="magenta", weight=3];
262 -> 639[label="",style="dashed", color="magenta", weight=3];
263[label="primModNatS0 (Succ xx30000) Zero True",fontsize=16,color="black",shape="box"];263 -> 274[label="",style="solid", color="black", weight=3];
264[label="primModNatS0 Zero (Succ xx31000) False",fontsize=16,color="black",shape="box"];264 -> 275[label="",style="solid", color="black", weight=3];
265[label="primModNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];265 -> 276[label="",style="solid", color="black", weight=3];
548[label="xx360",fontsize=16,color="green",shape="box"];549[label="xx350",fontsize=16,color="green",shape="box"];550[label="Succ (primDivNatS (primMinusNatS (Succ xx33) (Succ xx34)) (Succ (Succ xx34)))",fontsize=16,color="green",shape="box"];550 -> 558[label="",style="dashed", color="green", weight=3];
551[label="Zero",fontsize=16,color="green",shape="box"];636[label="xx31000",fontsize=16,color="green",shape="box"];637[label="xx31000",fontsize=16,color="green",shape="box"];638[label="xx30000",fontsize=16,color="green",shape="box"];639[label="xx30000",fontsize=16,color="green",shape="box"];635[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS xx59 xx60)",fontsize=16,color="burlywood",shape="triangle"];819[label="xx59/Succ xx590",fontsize=10,color="white",style="solid",shape="box"];635 -> 819[label="",style="solid", color="burlywood", weight=9];
819 -> 672[label="",style="solid", color="burlywood", weight=3];
820[label="xx59/Zero",fontsize=10,color="white",style="solid",shape="box"];635 -> 820[label="",style="solid", color="burlywood", weight=9];
820 -> 673[label="",style="solid", color="burlywood", weight=3];
274 -> 184[label="",style="dashed", color="red", weight=0];
274[label="primModNatS (primMinusNatS (Succ xx30000) Zero) (Succ Zero)",fontsize=16,color="magenta"];274 -> 289[label="",style="dashed", color="magenta", weight=3];
274 -> 290[label="",style="dashed", color="magenta", weight=3];
275[label="Succ Zero",fontsize=16,color="green",shape="box"];276 -> 184[label="",style="dashed", color="red", weight=0];
276[label="primModNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];276 -> 291[label="",style="dashed", color="magenta", weight=3];
276 -> 292[label="",style="dashed", color="magenta", weight=3];
558 -> 100[label="",style="dashed", color="red", weight=0];
558[label="primDivNatS (primMinusNatS (Succ xx33) (Succ xx34)) (Succ (Succ xx34))",fontsize=16,color="magenta"];558 -> 563[label="",style="dashed", color="magenta", weight=3];
558 -> 564[label="",style="dashed", color="magenta", weight=3];
672[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS (Succ xx590) xx60)",fontsize=16,color="burlywood",shape="box"];824[label="xx60/Succ xx600",fontsize=10,color="white",style="solid",shape="box"];672 -> 824[label="",style="solid", color="burlywood", weight=9];
824 -> 674[label="",style="solid", color="burlywood", weight=3];
825[label="xx60/Zero",fontsize=10,color="white",style="solid",shape="box"];672 -> 825[label="",style="solid", color="burlywood", weight=9];
825 -> 675[label="",style="solid", color="burlywood", weight=3];
673[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS Zero xx60)",fontsize=16,color="burlywood",shape="box"];826[label="xx60/Succ xx600",fontsize=10,color="white",style="solid",shape="box"];673 -> 826[label="",style="solid", color="burlywood", weight=9];
826 -> 676[label="",style="solid", color="burlywood", weight=3];
827[label="xx60/Zero",fontsize=10,color="white",style="solid",shape="box"];673 -> 827[label="",style="solid", color="burlywood", weight=9];
827 -> 677[label="",style="solid", color="burlywood", weight=3];
289[label="Zero",fontsize=16,color="green",shape="box"];290 -> 244[label="",style="dashed", color="red", weight=0];
290[label="primMinusNatS (Succ xx30000) Zero",fontsize=16,color="magenta"];290 -> 304[label="",style="dashed", color="magenta", weight=3];
291[label="Zero",fontsize=16,color="green",shape="box"];292 -> 246[label="",style="dashed", color="red", weight=0];
292[label="primMinusNatS Zero Zero",fontsize=16,color="magenta"];563[label="primMinusNatS (Succ xx33) (Succ xx34)",fontsize=16,color="black",shape="box"];563 -> 568[label="",style="solid", color="black", weight=3];
564[label="Succ xx34",fontsize=16,color="green",shape="box"];674[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS (Succ xx590) (Succ xx600))",fontsize=16,color="black",shape="box"];674 -> 678[label="",style="solid", color="black", weight=3];
675[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS (Succ xx590) Zero)",fontsize=16,color="black",shape="box"];675 -> 679[label="",style="solid", color="black", weight=3];
676[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS Zero (Succ xx600))",fontsize=16,color="black",shape="box"];676 -> 680[label="",style="solid", color="black", weight=3];
677[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];677 -> 681[label="",style="solid", color="black", weight=3];
304[label="xx30000",fontsize=16,color="green",shape="box"];568[label="primMinusNatS xx33 xx34",fontsize=16,color="burlywood",shape="triangle"];830[label="xx33/Succ xx330",fontsize=10,color="white",style="solid",shape="box"];568 -> 830[label="",style="solid", color="burlywood", weight=9];
830 -> 572[label="",style="solid", color="burlywood", weight=3];
831[label="xx33/Zero",fontsize=10,color="white",style="solid",shape="box"];568 -> 831[label="",style="solid", color="burlywood", weight=9];
831 -> 573[label="",style="solid", color="burlywood", weight=3];
678 -> 635[label="",style="dashed", color="red", weight=0];
678[label="primModNatS0 (Succ xx57) (Succ xx58) (primGEqNatS xx590 xx600)",fontsize=16,color="magenta"];678 -> 682[label="",style="dashed", color="magenta", weight=3];
678 -> 683[label="",style="dashed", color="magenta", weight=3];
679[label="primModNatS0 (Succ xx57) (Succ xx58) True",fontsize=16,color="black",shape="triangle"];679 -> 684[label="",style="solid", color="black", weight=3];
680[label="primModNatS0 (Succ xx57) (Succ xx58) False",fontsize=16,color="black",shape="box"];680 -> 685[label="",style="solid", color="black", weight=3];
681 -> 679[label="",style="dashed", color="red", weight=0];
681[label="primModNatS0 (Succ xx57) (Succ xx58) True",fontsize=16,color="magenta"];572[label="primMinusNatS (Succ xx330) xx34",fontsize=16,color="burlywood",shape="box"];834[label="xx34/Succ xx340",fontsize=10,color="white",style="solid",shape="box"];572 -> 834[label="",style="solid", color="burlywood", weight=9];
834 -> 576[label="",style="solid", color="burlywood", weight=3];
835[label="xx34/Zero",fontsize=10,color="white",style="solid",shape="box"];572 -> 835[label="",style="solid", color="burlywood", weight=9];
835 -> 577[label="",style="solid", color="burlywood", weight=3];
573[label="primMinusNatS Zero xx34",fontsize=16,color="burlywood",shape="box"];836[label="xx34/Succ xx340",fontsize=10,color="white",style="solid",shape="box"];573 -> 836[label="",style="solid", color="burlywood", weight=9];
836 -> 578[label="",style="solid", color="burlywood", weight=3];
837[label="xx34/Zero",fontsize=10,color="white",style="solid",shape="box"];573 -> 837[label="",style="solid", color="burlywood", weight=9];
837 -> 579[label="",style="solid", color="burlywood", weight=3];
682[label="xx600",fontsize=16,color="green",shape="box"];683[label="xx590",fontsize=16,color="green",shape="box"];684 -> 184[label="",style="dashed", color="red", weight=0];
684[label="primModNatS (primMinusNatS (Succ xx57) (Succ xx58)) (Succ (Succ xx58))",fontsize=16,color="magenta"];684 -> 686[label="",style="dashed", color="magenta", weight=3];
684 -> 687[label="",style="dashed", color="magenta", weight=3];
685[label="Succ (Succ xx57)",fontsize=16,color="green",shape="box"];576[label="primMinusNatS (Succ xx330) (Succ xx340)",fontsize=16,color="black",shape="box"];576 -> 616[label="",style="solid", color="black", weight=3];
577[label="primMinusNatS (Succ xx330) Zero",fontsize=16,color="black",shape="box"];577 -> 617[label="",style="solid", color="black", weight=3];
578[label="primMinusNatS Zero (Succ xx340)",fontsize=16,color="black",shape="box"];578 -> 618[label="",style="solid", color="black", weight=3];
579[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="box"];579 -> 619[label="",style="solid", color="black", weight=3];
686[label="Succ xx58",fontsize=16,color="green",shape="box"];687 -> 568[label="",style="dashed", color="red", weight=0];
687[label="primMinusNatS (Succ xx57) (Succ xx58)",fontsize=16,color="magenta"];687 -> 688[label="",style="dashed", color="magenta", weight=3];
687 -> 689[label="",style="dashed", color="magenta", weight=3];
616 -> 568[label="",style="dashed", color="red", weight=0];
616[label="primMinusNatS xx330 xx340",fontsize=16,color="magenta"];616 -> 627[label="",style="dashed", color="magenta", weight=3];
616 -> 628[label="",style="dashed", color="magenta", weight=3];
617[label="Succ xx330",fontsize=16,color="green",shape="box"];618[label="Zero",fontsize=16,color="green",shape="box"];619[label="Zero",fontsize=16,color="green",shape="box"];688[label="Succ xx57",fontsize=16,color="green",shape="box"];689[label="Succ xx58",fontsize=16,color="green",shape="box"];627[label="xx330",fontsize=16,color="green",shape="box"];628[label="xx340",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xx3000), Succ(xx400)) → new_primPlusNat(xx3000, xx400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(xx3000), Succ(xx400)) → new_primPlusNat(xx3000, xx400)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xx3100)) → new_primMulNat(xx3100)

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(xx3100)) → new_primMulNat(xx3100)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(xx3000), Succ(xx400)) → new_primMinusNat(xx3000, xx400)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(xx3000), Succ(xx400)) → new_primMinusNat(xx3000, xx400)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(xx330), Succ(xx340)) → new_primMinusNatS(xx330, xx340)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNatS(Succ(xx330), Succ(xx340)) → new_primMinusNatS(xx330, xx340)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS(Succ(Zero), Zero) → new_primModNatS(new_primMinusNatS1, Zero)
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS(Succ(Succ(xx30000)), Zero) → new_primModNatS(new_primMinusNatS0(xx30000), Zero)
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)
new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS1 → Zero
new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(xx30000)), Zero) → new_primModNatS(new_primMinusNatS0(xx30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS1 → Zero
new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(xx30000)), Zero) → new_primModNatS(new_primMinusNatS0(xx30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(xx30000)), Zero) → new_primModNatS(new_primMinusNatS0(xx30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primModNatS(Succ(Succ(xx30000)), Zero) → new_primModNatS(new_primMinusNatS0(xx30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(xx30000) → Succ(xx30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primMinusNatS0(x₁)) = 2 + 2·x₁
POL(new_primModNatS(x₁, x₂)) = x₁ + x₂

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                                ↳ QDP

                                                  ↳ PisEmptyProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)
new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS1 → Zero
new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)
new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)
new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58)) at position [0] we obtained the following new rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)
new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58))
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(Succ(xx57), Succ(xx58)), Succ(xx58)) at position [0] we obtained the following new rules:

new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))
new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primModNatS0(xx57, xx58, Succ(xx590), Zero) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))
new_primModNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primModNatS0(xx30000, xx31000, xx30000, xx31000)
new_primModNatS0(xx57, xx58, Zero, Zero) → new_primModNatS00(xx57, xx58)

The remaining pairs can at least be oriented weakly.

new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primMinusNatS2(x₁, x₂)) = x₁
POL(new_primModNatS(x₁, x₂)) = x₁
POL(new_primModNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁
POL(new_primModNatS00(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(xx57, xx58) → new_primModNatS(new_primMinusNatS2(xx57, xx58), Succ(xx58))
new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ UsableRulesProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ UsableRulesProof

                                                                ↳ QDP

                                                                  ↳ QReductionProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ UsableRulesProof

                                                                ↳ QDP

                                                                  ↳ QReductionProof

                                                                    ↳ QDP

                                                                      ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)

From the DPs we obtained the following set of size-change graphs:

new_primModNatS0(xx57, xx58, Succ(xx590), Succ(xx600)) → new_primModNatS0(xx57, xx58, xx590, xx600)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Zero, Zero) → new_primDivNatS00(xx33, xx34)
new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
new_primDivNatS0(xx33, xx34, Succ(xx350), Zero) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primDivNatS0(xx30000, xx31000, xx30000, xx31000)
new_primDivNatS00(xx33, xx34) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS(Succ(Succ(xx30000)), Zero) → new_primDivNatS(new_primMinusNatS0(xx30000), Zero)
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS1, Zero)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS1 → Zero
new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(xx30000)), Zero) → new_primDivNatS(new_primMinusNatS0(xx30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS1 → Zero
new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(xx30000)), Zero) → new_primDivNatS(new_primMinusNatS0(xx30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(xx30000)), Zero) → new_primDivNatS(new_primMinusNatS0(xx30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

new_primDivNatS(Succ(Succ(xx30000)), Zero) → new_primDivNatS(new_primMinusNatS0(xx30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(xx30000) → Succ(xx30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁ + x₂
POL(new_primMinusNatS0(x₁)) = 2 + 2·x₁

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                                ↳ QDP

                                                  ↳ PisEmptyProof

                                    ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Zero, Zero) → new_primDivNatS00(xx33, xx34)
new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
new_primDivNatS0(xx33, xx34, Succ(xx350), Zero) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primDivNatS0(xx30000, xx31000, xx30000, xx31000)
new_primDivNatS00(xx33, xx34) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS1 → Zero
new_primMinusNatS0(xx30000) → Succ(xx30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Zero, Zero) → new_primDivNatS00(xx33, xx34)
new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
new_primDivNatS0(xx33, xx34, Succ(xx350), Zero) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primDivNatS0(xx30000, xx31000, xx30000, xx31000)
new_primDivNatS00(xx33, xx34) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Zero, Zero) → new_primDivNatS00(xx33, xx34)
new_primDivNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primDivNatS0(xx30000, xx31000, xx30000, xx31000)
new_primDivNatS0(xx33, xx34, Succ(xx350), Zero) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
new_primDivNatS00(xx33, xx34) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS(Succ(Succ(xx30000)), Succ(xx31000)) → new_primDivNatS0(xx30000, xx31000, xx30000, xx31000)

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(xx33, xx34, Zero, Zero) → new_primDivNatS00(xx33, xx34)
new_primDivNatS0(xx33, xx34, Succ(xx350), Zero) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
new_primDivNatS00(xx33, xx34) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁ + x₂
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂
POL(new_primDivNatS00(x₁, x₂)) = 1 + x₁ + x₂
POL(new_primMinusNatS2(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Zero) → Zero

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Zero, Zero) → new_primDivNatS00(xx33, xx34)
new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
new_primDivNatS0(xx33, xx34, Succ(xx350), Zero) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))
new_primDivNatS00(xx33, xx34) → new_primDivNatS(new_primMinusNatS2(xx33, xx34), Succ(xx34))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(xx330), Succ(xx340)) → new_primMinusNatS2(xx330, xx340)
new_primMinusNatS2(Zero, Succ(xx340)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(xx330), Zero) → Succ(xx330)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ QReductionProof

                                                            ↳ QDP

                                                              ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(xx33, xx34, Succ(xx350), Succ(xx360)) → new_primDivNatS0(xx33, xx34, xx350, xx360)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x